E,X1,X2:Type, info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), pred?:(E(?E)).
wellfounded{i:l}
wellfounded(E; e,e'.(((first(e'))) c (e = pred(e')  E)))
 (e:E. ((first(e)))  (loc(pred(e)) = loc(e)  Id))
 (e,e':E. (loc(e) = loc(e')  Id)  (pred?(e) = pred?(e'))  (e = e'))
 (e,e':E.
 (loc(e) = loc(e')  Id)
  ((e rel_plus(E; (e,e'. ((first(e'))) c (e = pred(e')))) e')
   (e = e')
   (e' rel_plus(E; (e,e'. ((first(e'))) c (e = pred(e')))) e))) 

latex

Definitions

prop{i:l}, t  T, Unit, Type, left + right, x:AB(x), x:A  B(x), rel_plus(T; R), x f y, P  Q, void, isect(A; x.B(x)), top, subtype(S; T), suptype(S; T), x,y. t(x;y), wellfounded{i:l}(A; x,y.R(x;y)), IdLnk, pred(e), s = t, first(e), b, A, A c B, x.A(x), rel_star(T; R), f(a), loc(e), Id, P  Q, x:A. B(x), False, decidable(P), guard(T), x. t(x), (i = j), rel_exp(T; R; n), A  B, a < b, {x:A| B(x)} , , , x:A. B(x), #$n, , inr x , True, <a, b>, sq_type(T), sqequal(s; t), b, , P  Q, P  Q, , inl x , -n, n + m, n - m, trans(T; x,y.E(x;y))

Lemmas

rel plus trans, rel-rel-plus, nat plus inc, bool cases, eqtt to assert, bool sq, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, decidable int equal, rel plus wf, rel star transitivity, rel rel star, false wf, true wf, it wf, le wf, rel exp wf, rel star wf, decidable assert, IdLnk wf, wellfounded wf, not wf, assert wf, first wf, pred wf, top wf, Id wf, loc wf, unit wf